(declare-sort S0 0)

(declare-const S0-0 S0)
(assert (fmf.card S0-0 1))
(assert (fmf.card S0-0 4))
(check-sat)
